

LEMMA

Inverse non-tangential proper part implies inverse proper part.
=============================
Step 1

? (all x (all y ((ntpp-1 x y) => (pp-1 x y))))


> revsk
=============================
Step 2

? ((~ (ntpp-1 c622163 c622162)) v (pp-1 c622163 c622162))


> hypdisj
=============================
Step 3

? (pp-1 c622163 c622162)

1. (ntpp-1 c622163 c622162)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c622162 c622163)

1. (~ (pp-1 c622163 c622162))
2. (ntpp-1 c622163 c622162)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 5

? (ntpp c622162 c622163)

1. (~ (pp c622162 c622163))
2. (~ (pp-1 c622163 c622162))
3. (ntpp-1 c622163 c622162)

> ((ntpp Y X) <-- (ntpp-1 X Y))
=============================
Step 6

? (ntpp-1 c622163 c622162)

1. (~ (ntpp c622162 c622163))
2. (~ (pp c622162 c622163))
3. (~ (pp-1 c622163 c622162))
4. (ntpp-1 c622163 c622162)

> hyp


LEMMA

Inverse proper part implies inverse parthood.
=============================
Step 1

? (all x (all y ((pp-1 x y) => (p-1 x y))))


> revsk
=============================
Step 2

? ((~ (pp-1 c627292 c627291)) v (p-1 c627292 c627291))


> hypdisj
=============================
Step 3

? (p-1 c627292 c627291)

1. (pp-1 c627292 c627291)

> ((p-1 Y X) <-- (p X Y))
=============================
Step 4

? (p c627291 c627292)

1. (~ (p-1 c627292 c627291))
2. (pp-1 c627292 c627291)

> ((p X Y) <-- (pp X Y))
=============================
Step 5

? (pp c627291 c627292)

1. (~ (p c627291 c627292))
2. (~ (p-1 c627292 c627291))
3. (pp-1 c627292 c627291)

> ((pp Y X) <-- (pp-1 X Y))
=============================
Step 6

? (pp-1 c627292 c627291)

1. (~ (pp c627291 c627292))
2. (~ (p c627291 c627292))
3. (~ (p-1 c627292 c627291))
4. (pp-1 c627292 c627291)

> hyp


LEMMA

External connection excludes overlap.
=============================
Step 1

? (all x (all y ((ec x y) => (~ (o x y)))))


> revsk
=============================
Step 2

? ((~ (ec c632477 c632476)) v (~ (o c632477 c632476)))


> hypdisj
=============================
Step 3

? (~ (o c632477 c632476))

1. (ec c632477 c632476)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 4

? (ec c632477 c632476)

1. (o c632477 c632476)
2. (ec c632477 c632476)

> hyp


LEMMA

If y non-tangentially contains z, nothing can be externally connected to both y and z.
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp-1 y z)) => (~ (ec x z))))))


> revsk
=============================
Step 2

? (((~ (ec c637720 c637719)) v (~ (ntpp-1 c637719 c637718))) v (~ (ec c637720 c637718)))


> hypdisj
=============================
Step 3

? (~ (ec c637720 c637718))

1. (ntpp-1 c637719 c637718)
2. (ec c637720 c637719)

> ((~ (ec Y X)) <-- (ntpp X Z) (ec Y Z))
|=============================
|Step 4
|
|? (ntpp c637718 Var26)
|
|1. (ec c637720 c637718)
|2. (ntpp-1 c637719 c637718)
|3. (ec c637720 c637719)
|
|> ((ntpp Y X) <-- (ntpp-1 X Y))
|=============================
|Step 5
|
|? (ntpp-1 Var26 c637718)
|
|1. (~ (ntpp c637718 Var26))
|2. (ec c637720 c637718)
|3. (ntpp-1 c637719 c637718)
|4. (ec c637720 c637719)
|
|> hyp
=============================
Step 6

? (ec c637720 c637719)

1. (ec c637720 c637718)
2. (ntpp-1 c637719 c637718)
3. (ec c637720 c637719)

> hyp


LEMMA

Under the hypotheses, if x is connected to z then x does not overlap z.
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (ntpp-1 y z)) & (c x z)) => (~ (o x z))))))


> revsk
=============================
Step 2

? ((((~ (ec c643119 c643118)) v (~ (ntpp-1 c643118 c643117))) v (~ (c c643119 c643117))) v (~ (o c643119 c643117)))


> hypdisj
=============================
Step 3

? (~ (o c643119 c643117))

1. (c c643119 c643117)
2. (ntpp-1 c643118 c643117)
3. (ec c643119 c643118)

> ((~ (o Y X)) <-- (~ (p (f637777 Y X) Y)))
=============================
Step 4

? (~ (p (f637777 c643119 c643117) c643119))

1. (o c643119 c643117)
2. (c c643119 c643117)
3. (ntpp-1 c643118 c643117)
4. (ec c643119 c643118)

> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
|=============================
|Step 5
|
|? (p (f637777 c643119 c643117) Var53)
|
|1. (p (f637777 c643119 c643117) c643119)
|2. (o c643119 c643117)
|3. (c c643119 c643117)
|4. (ntpp-1 c643118 c643117)
|5. (ec c643119 c643118)
|
|> ((p X Z) <-- (c (f637760 X Z Y) Z))
|=============================
|Step 6
|
|? (c (f637760 (f637777 c643119 c643117) Var53 Var56) Var53)
|
|1. (~ (p (f637777 c643119 c643117) Var53))
|2. (p (f637777 c643119 c643117) c643119)
|3. (o c643119 c643117)
|4. (c c643119 c643117)
|5. (ntpp-1 c643118 c643117)
|6. (ec c643119 c643118)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 7
||
||? (p Var59 Var53)
||
||1. (~ (c (f637760 (f637777 c643119 c643117) Var53 Var56) Var53))
||2. (~ (p (f637777 c643119 c643117) Var53))
||3. (p (f637777 c643119 c643117) c643119)
||4. (o c643119 c643117)
||5. (c c643119 c643117)
||6. (ntpp-1 c643118 c643117)
||7. (ec c643119 c643118)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 8
||
||? (pp Var59 Var53)
||
||1. (~ (p Var59 Var53))
||2. (~ (c (f637760 (f637777 c643119 c643117) Var53 Var56) Var53))
||3. (~ (p (f637777 c643119 c643117) Var53))
||4. (p (f637777 c643119 c643117) c643119)
||5. (o c643119 c643117)
||6. (c c643119 c643117)
||7. (ntpp-1 c643118 c643117)
||8. (ec c643119 c643118)
||
||> ((pp X Y) <-- (ntpp X Y))
||=============================
||Step 9
||
||? (ntpp Var59 Var53)
||
||1. (~ (pp Var59 Var53))
||2. (~ (p Var59 Var53))
||3. (~ (c (f637760 (f637777 c643119 c643117) Var53 Var56) Var53))
||4. (~ (p (f637777 c643119 c643117) Var53))
||5. (p (f637777 c643119 c643117) c643119)
||6. (o c643119 c643117)
||7. (c c643119 c643117)
||8. (ntpp-1 c643118 c643117)
||9. (ec c643119 c643118)
||
||> ((ntpp Y X) <-- (ntpp-1 X Y))
||=============================
||Step 10
||
||? (ntpp-1 Var53 Var59)
||
||1. (~ (ntpp Var59 Var53))
||2. (~ (pp Var59 Var53))
||3. (~ (p Var59 Var53))
||4. (~ (c (f637760 (f637777 c643119 c643117) Var53 Var56) Var53))
||5. (~ (p (f637777 c643119 c643117) Var53))
||6. (p (f637777 c643119 c643117) c643119)
||7. (o c643119 c643117)
||8. (c c643119 c643117)
||9. (ntpp-1 c643118 c643117)
||10. (ec c643119 c643118)
||
||> hyp
|=============================
|Step 11
|
|? (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643117)
|
|1. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643118))
|2. (~ (p (f637777 c643119 c643117) c643118))
|3. (p (f637777 c643119 c643117) c643119)
|4. (o c643119 c643117)
|5. (c c643119 c643117)
|6. (ntpp-1 c643118 c643117)
|7. (ec c643119 c643118)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 12
||
||? (p (f637777 Var72 c643117) c643117)
||
||1. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643117))
||2. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643118))
||3. (~ (p (f637777 c643119 c643117) c643118))
||4. (p (f637777 c643119 c643117) c643119)
||5. (o c643119 c643117)
||6. (c c643119 c643117)
||7. (ntpp-1 c643118 c643117)
||8. (ec c643119 c643118)
||
||> ((p (f637777 X Y) Y) <-- (o X Y))
||=============================
||Step 13
||
||? (o Var72 c643117)
||
||1. (~ (p (f637777 Var72 c643117) c643117))
||2. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643117))
||3. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643118))
||4. (~ (p (f637777 c643119 c643117) c643118))
||5. (p (f637777 c643119 c643117) c643119)
||6. (o c643119 c643117)
||7. (c c643119 c643117)
||8. (ntpp-1 c643118 c643117)
||9. (ec c643119 c643118)
||
||> hyp
|=============================
|Step 14
|
|? (c (f637760 (f637777 c643119 c643117) c643118 Var56) (f637777 c643119 c643117))
|
|1. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643117))
|2. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643118))
|3. (~ (p (f637777 c643119 c643117) c643118))
|4. (p (f637777 c643119 c643117) c643119)
|5. (o c643119 c643117)
|6. (c c643119 c643117)
|7. (ntpp-1 c643118 c643117)
|8. (ec c643119 c643118)
|
|> ((c (f637760 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 15
|
|? (~ (p (f637777 c643119 c643117) c643118))
|
|1. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) (f637777 c643119 c643117)))
|2. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643117))
|3. (~ (c (f637760 (f637777 c643119 c643117) c643118 Var56) c643118))
|4. (~ (p (f637777 c643119 c643117) c643118))
|5. (p (f637777 c643119 c643117) c643119)
|6. (o c643119 c643117)
|7. (c c643119 c643117)
|8. (ntpp-1 c643118 c643117)
|9. (ec c643119 c643118)
|
|> hyp
=============================
Step 16

? (~ (o c643119 c643118))

1. (p (f637777 c643119 c643117) c643119)
2. (o c643119 c643117)
3. (c c643119 c643117)
4. (ntpp-1 c643118 c643117)
5. (ec c643119 c643118)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 17

? (ec c643119 c643118)

1. (o c643119 c643118)
2. (p (f637777 c643119 c643117) c643119)
3. (o c643119 c643117)
4. (c c643119 c643117)
5. (ntpp-1 c643118 c643117)
6. (ec c643119 c643118)

> hyp


LEMMA

Connected plus non-overlap gives ec(x,z).
=============================
Step 1

? (all x (all y (all z ((((ec x y) & (ntpp-1 y z)) & (c x z)) => (ec x z)))))


> revsk
=============================
Step 2

? ((((~ (ec c648784 c648783)) v (~ (ntpp-1 c648783 c648782))) v (~ (c c648784 c648782))) v (ec c648784 c648782))


> hypdisj
=============================
Step 3

? (ec c648784 c648782)

1. (c c648784 c648782)
2. (ntpp-1 c648783 c648782)
3. (ec c648784 c648783)

> ((ec X Y) <-- (c X Y) (~ (o X Y)))
|=============================
|Step 4
|
|? (c c648784 c648782)
|
|1. (~ (ec c648784 c648782))
|2. (c c648784 c648782)
|3. (ntpp-1 c648783 c648782)
|4. (ec c648784 c648783)
|
|> hyp
=============================
Step 5

? (~ (o c648784 c648782))

1. (~ (ec c648784 c648782))
2. (c c648784 c648782)
3. (ntpp-1 c648783 c648782)
4. (ec c648784 c648783)

> ((~ (o Y Z)) <-- (ec Y X) (ntpp-1 X Z) (c Y Z))
||=============================
||Step 6
||
||? (ec c648784 Var31)
||
||1. (o c648784 c648782)
||2. (~ (ec c648784 c648782))
||3. (c c648784 c648782)
||4. (ntpp-1 c648783 c648782)
||5. (ec c648784 c648783)
||
||> hyp
|=============================
|Step 7
|
|? (ntpp-1 c648783 c648782)
|
|1. (o c648784 c648782)
|2. (~ (ec c648784 c648782))
|3. (c c648784 c648782)
|4. (ntpp-1 c648783 c648782)
|5. (ec c648784 c648783)
|
|> hyp
=============================
Step 8

? (c c648784 c648782)

1. (o c648784 c648782)
2. (~ (ec c648784 c648782))
3. (c c648784 c648782)
4. (ntpp-1 c648783 c648782)
5. (ec c648784 c648783)

> hyp


LEMMA

Split on dc(x,z) or c(x,z). In the connected case use Lemma6 to get ec(x,z), contradicting Lemma4. Hence dc(x,z).
=============================
Step 1

? (all x (all y (all z (((ec x y) & (ntpp-1 y z)) => (dc x z)))))


> revsk
=============================
Step 2

? (((~ (ec c654715 c654714)) v (~ (ntpp-1 c654714 c654713))) v (dc c654715 c654713))


> hypdisj
=============================
Step 3

? (dc c654715 c654713)

1. (ntpp-1 c654714 c654713)
2. (ec c654715 c654714)

> ((dc X Y) <-- (~ (c X Y)))
=============================
Step 4

? (~ (c c654715 c654713))

1. (~ (dc c654715 c654713))
2. (ntpp-1 c654714 c654713)
3. (ec c654715 c654714)

> ((~ (c X Y)) <-- (~ (o X Y)) (~ (ec X Y)))
|=============================
|Step 5
|
|? (~ (o c654715 c654713))
|
|1. (c c654715 c654713)
|2. (~ (dc c654715 c654713))
|3. (ntpp-1 c654714 c654713)
|4. (ec c654715 c654714)
|
|> ((~ (o Y Z)) <-- (ec Y X) (ntpp-1 X Z) (c Y Z))
|||=============================
|||Step 6
|||
|||? (ec c654715 Var38)
|||
|||1. (o c654715 c654713)
|||2. (c c654715 c654713)
|||3. (~ (dc c654715 c654713))
|||4. (ntpp-1 c654714 c654713)
|||5. (ec c654715 c654714)
|||
|||> hyp
||=============================
||Step 7
||
||? (ntpp-1 c654714 c654713)
||
||1. (o c654715 c654713)
||2. (c c654715 c654713)
||3. (~ (dc c654715 c654713))
||4. (ntpp-1 c654714 c654713)
||5. (ec c654715 c654714)
||
||> hyp
|=============================
|Step 8
|
|? (c c654715 c654713)
|
|1. (o c654715 c654713)
|2. (c c654715 c654713)
|3. (~ (dc c654715 c654713))
|4. (ntpp-1 c654714 c654713)
|5. (ec c654715 c654714)
|
|> hyp
=============================
Step 9

? (~ (ec c654715 c654713))

1. (c c654715 c654713)
2. (~ (dc c654715 c654713))
3. (ntpp-1 c654714 c654713)
4. (ec c654715 c654714)

> ((~ (ec X Z)) <-- (ec X Y) (ntpp-1 Y Z))
|=============================
|Step 10
|
|? (ec c654715 Var44)
|
|1. (ec c654715 c654713)
|2. (c c654715 c654713)
|3. (~ (dc c654715 c654713))
|4. (ntpp-1 c654714 c654713)
|5. (ec c654715 c654714)
|
|> hyp
=============================
Step 11

? (ntpp-1 c654713 c654713)

1. (ec c654715 c654713)
2. (c c654715 c654713)
3. (~ (dc c654715 c654713))
4. (ntpp-1 c654714 c654713)
5. (ec c654715 c654714)

> hyp
=============================
Step 12

? (ntpp-1 c654714 c654713)

1. (ec c654715 c654713)
2. (c c654715 c654713)
3. (~ (dc c654715 c654713))
4. (ntpp-1 c654714 c654713)
5. (ec c654715 c654714)

> hyp
